Skolem Function

释义 Definition

Skolem function（斯科伦函数）：在一阶逻辑/模型论中，用来消去存在量词（∃）的函数。直观上，它为“对每个 \(x\) 都存在某个 \(y\)”里的 \(y\) 提供一个依赖于 \(x\) 的明确“见证”（即 \(y = f(x)\)），从而把公式改写为只含全称量词的形式（常见于Skolemization 斯科伦化）。

发音 Pronunciation (IPA)

/ˈskoʊləm ˈfʌŋkʃən/

例句 Examples

If every student has a mentor, a Skolem function can assign each student a mentor.
如果每个学生都有导师，斯科伦函数就可以为每个学生指派一个导师。

In Skolemization, we replace existential variables with Skolem functions whose arguments are the surrounding universally quantified variables.
在斯科伦化中，我们用斯科伦函数替换存在量词下的变量，而该函数的自变量就是外层的全称量词变量。

词源 Etymology

“Skolem”来自挪威逻辑学家 Thoralf Skolem（托拉尔夫·斯科伦） 的姓氏；“function”源自拉丁语 functio（执行、作用）。该术语因斯科伦在模型论与一阶逻辑中的相关工作而得名，用于描述将“存在对象”的选择用函数形式固定下来的方法。

相关词 Related Words

• Skolemization
• First-Order Logic
• Existential Quantifier
• Universal Quantifier
• Model Theory
• Witness
• Function Symbol
• Herbrand Universe
• Axiom Of Choice

文学与经典著作 Literary Works

• Thoralf Skolem 的论文与著作（涉及斯科伦正规形与可满足性思想的来源背景）
• Elliott Mendelson, Introduction to Mathematical Logic（常在量词消去/斯科伦化部分出现该术语）
• Chang & Keisler, Model Theory（模型论标准教材，讨论斯科伦函数与斯科伦闭包等概念）
• Dirk van Dalen, Logic and Structure（逻辑教材中讲解斯科伦化与相关变换时常出现）